K{-}implements($S$;${\it equiv}$;${\it pr}$;${\it kpr}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$K{-}sem($S$;${\it equiv}$)(${\it kpr}$,$S$(${\it pr}$))